/* Copyright 2002 -- Ira R. Forman and Nate Forman */ 
/**
 * This transformation creates a subclass that checks the invariant of a class
 * whenever a nonstatic method is called (and on the return, too). 
 * The invariant is a method that takes no parameters and returns a boolean. 
 * The name of the invariant method is given after the -invariant flag.
 * If the -invariant flag does not appear in the args array, the
 * transformation assumes that the invariant method is named "invariant".
 */
//start extract C2InvariantCheckingC
package c2c;
import java.lang.reflect.*;
import mopex.*;

public class C2InvariantCheckingC extends C2IdentitySubclassOfC {
    
    protected Method  invMethod;
    
    static public void main( String[] args ) {
	new C2InvariantCheckingC().createClass( args );
    }
    
    protected String generateClassNamePrefix() {
	return "InvariantChecking" + super.generateClassNamePrefix();
    }
    
    protected void checkAndProcessArgs( Args args ) {                      //#1
	super.checkAndProcessArgs( args );

	try {
	    invMethod = inputClassObject.getMethod( "invariant", null );
	} catch(NoSuchMethodException e){
	    throw new C2CException(e);
	}
	if ( invMethod.getReturnType() != boolean.class )
	    throw new C2CException("invariant return not boolean");

	if ( inputClassObject.getPackage() != null ) {
	    if ( !inputClassObject.getPackage().getName().equals(packageName) )
		throw new C2CException( "input class in different package" );
	} else if ( packageName != null ) {
	    throw new C2CException( "Input class in different package" );
	}

	if (Mopex.getMethodsLackingImplementation(inputClassObject).length!=0)
	    setAbstract();
    }
    
//stop extract C2InvariantCheckingC
//      protected String getClassLevelJavadoc() {
//  	return "/**\n" 
//  	    +  " * Checks the invariant for this class before and after\n" 
//  	    +  " * each nonstatic method is called.\n" 
//  	    +  " */\n";
//      }
    
    /**
     * For each method that is neither private nor static nor abstract nor final,
     * a cooperative override is added that checks the invariant.  To do so, a private
     * method checkInvariant is added to the class.  This private method checks
     * the invariant, if invariantCheckInProgress is false.  This boolean prevents
     * a dispatch loop in the event that the invariant method is implemented using
     * method calls on the object.
     */
//start extract C2InvariantCheckingC
    protected String generateMethods() {                                    //#2

	int mods = Modifier.STATIC | Modifier.ABSTRACT 
	         | Modifier.FINAL | Modifier.PRIVATE;

	Method[] nsMethods = Mopex.selectMethods( inputClassObject, 
						  0, 
						  mods, 
						  Object.class );

	String result = generateCheckInvariant();

	String wrapperCode 
	    = "    assert checkInvariant() : \"invariant failure\";\n";
	for ( int i = 0; i < nsMethods.length; i++ ) {
	    if ( !invMethod.equals( nsMethods[i]) ) {
		int mods2 = Mopex.getModifiersWithout( nsMethods[i], 
						       Modifier.NATIVE );
		result += Modifier.toString(mods2) + " "
		        + Mopex.createCooperativeWrapper( nsMethods[i], 
							  wrapperCode, 
							  wrapperCode );
	    }
	}
	return super.generateMethods() + result;
    }

    private String generateCheckInvariant() {                              //#3
	return "private boolean checkInvariant() {\n"
	     + "    StackTraceElement[] ste\n"
	     + "        = (new Throwable()).getStackTrace();\n"
	     + "    String className = this.getClass().getName();\n"
	     + "    String mName = \"checkInvariant\";\n"
	     + "    for ( int i = 1; i < ste.length; i++ ) {\n"
	     + "        if ( ste[i].getClassName().equals(className)\n"
	     + "             && ste[i].getMethodName().equals(mName) )\n"
	     + "            return true;\n"
	     + "        }\n"
	     + "    return this.invariant();\n"
	     + "}\n";
    }
}
//stop extract C2InvariantCheckingC
